Step of Proof: int_lt_to_int_upper
9,38
postcript
pdf
Inference at
*
1
I
of proof for Lemma
int
lt
to
int
upper
:
i
:
,
A
:({
i
+ 1...}
). (
j
:
. (
i
<
j
)
A
(
j
))
(
j
:{
i
+ 1...}.
A
(
j
))
latex
by ((GenUnivCD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
1.
i
:
C1:
2.
A
: {
i
+ 1...}
C1:
3.
j
:
. (
i
<
j
)
A
(
j
)
C1:
4.
j
: {
i
+ 1...}
C1:
A
(
j
)
C
2
:
C2:
1.
i
:
C2:
2.
A
: {
i
+ 1...}
C2:
3.
j
:{
i
+ 1...}.
A
(
j
)
C2:
4.
j
:
C2:
5.
i
<
j
C2:
A
(
j
)
C
.
Definitions
False
,
A
,
A
B
,
t
T
,
P
Q
,
P
Q
,
x
(
s
)
,
P
Q
,
P
Q
,
,
{
i
...}
,
x
:
A
.
B
(
x
)
Lemmas
le
wf
,
int
upper
wf
origin